A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A), x:A, P:(a:{a:A| a  dom(f) }B(a)Prop).
(z != f(x)  P(x,z))  Prop 

latex

Definitions	z != f(x)  P(a;z), x(s1,s2), f(x), x  dom(f), Prop, b, x. t(x), P  Q, strong-subtype(A;B), x:A. B(x), EqDecider(T), a:A fp B(a), x(s), Top, t  T
Lemmas	strong-subtype-self, top wf, subtype-fpf3, fpf wf, deq wf, fpf-dom wf, assert wf, fpf-ap wf